Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		0(#)	→ #
2:		# + x	→ x
3:		x + #	→ x
4:		0(x) + 0(y)	→ 0(x + y)
5:		0(x) + 1(y)	→ 1(x + y)
6:		1(x) + 0(y)	→ 1(x + y)
7:		1(x) + 1(y)	→ 0((x + y) + 1(#))
8:		(x + y) + z	→ x + (y + z)
9:		# - x	→ #
10:		x - #	→ x
11:		0(x) - 0(y)	→ 0(x - y)
12:		0(x) - 1(y)	→ 1((x - y) - 1(#))
13:		1(x) - 0(y)	→ 1(x - y)
14:		1(x) - 1(y)	→ 0(x - y)
15:		not(true)	→ false
16:		not(false)	→ true
17:		if(true,x,y)	→ x
18:		if(false,x,y)	→ y
19:		ge(0(x),0(y))	→ ge(x,y)
20:		ge(0(x),1(y))	→ not(ge(y,x))
21:		ge(1(x),0(y))	→ ge(x,y)
22:		ge(1(x),1(y))	→ ge(x,y)
23:		ge(x,#)	→ true
24:		ge(#,0(x))	→ ge(#,x)
25:		ge(#,1(x))	→ false
26:		log(x)	→ log'(x) - 1(#)
27:		log'(#)	→ #
28:		log'(1(x))	→ log'(x) + 1(#)
29:		log'(0(x))	→ if(ge(x,1(#)),log'(x) + 1(#),#)

There are 30 dependency pairs:


30:		0(x) +# 0(y)	→ 0#(x + y)
31:		0(x) +# 0(y)	→ x +# y
32:		0(x) +# 1(y)	→ x +# y
33:		1(x) +# 0(y)	→ x +# y
34:		1(x) +# 1(y)	→ 0#((x + y) + 1(#))
35:		1(x) +# 1(y)	→ (x + y) +# 1(#)
36:		1(x) +# 1(y)	→ x +# y
37:		(x + y) +# z	→ x +# (y + z)
38:		(x + y) +# z	→ y +# z
39:		0(x) -# 0(y)	→ 0#(x - y)
40:		0(x) -# 0(y)	→ x -# y
41:		0(x) -# 1(y)	→ (x - y) -# 1(#)
42:		0(x) -# 1(y)	→ x -# y
43:		1(x) -# 0(y)	→ x -# y
44:		1(x) -# 1(y)	→ 0#(x - y)
45:		1(x) -# 1(y)	→ x -# y
46:		GE(0(x),0(y))	→ GE(x,y)
47:		GE(0(x),1(y))	→ NOT(ge(y,x))
48:		GE(0(x),1(y))	→ GE(y,x)
49:		GE(1(x),0(y))	→ GE(x,y)
50:		GE(1(x),1(y))	→ GE(x,y)
51:		GE(#,0(x))	→ GE(#,x)
52:		LOG(x)	→ log'(x) -# 1(#)
53:		LOG(x)	→ LOG'(x)
54:		LOG'(1(x))	→ log'(x) +# 1(#)
55:		LOG'(1(x))	→ LOG'(x)
56:		LOG'(0(x))	→ IF(ge(x,1(#)),log'(x) + 1(#),#)
57:		LOG'(0(x))	→ GE(x,1(#))
58:		LOG'(0(x))	→ log'(x) +# 1(#)
59:		LOG'(0(x))	→ LOG'(x)

The approximated dependency graph contains 5 SCCs: {51}, {31-33,35-38}, {40-43,45}, {46,48-50} and {55,59}.

Consider the SCC {51}. There are no usable rules. By taking the AF π with π(GE) = 2 together with the lexicographic path order with empty precedence, rule 51 is strictly decreasing.

Consider the SCC {31-33,35-38}. The usable rules are {1-8}. The constraints could not be solved.

Consider the SCC {40-43,45}. The usable rules are {1,9-14}. By taking the AF π with π(-) = π(-#) = 1 together with the lexicographic path order with precedence 1 ≈ 0, the rules in {9-14} are weakly decreasing and the rules in {1,40-43,45} are strictly decreasing.

Consider the SCC {46,48-50}. There are no usable rules. The constraints could not be solved.

Consider the SCC {55,59}. There are no usable rules. By taking the AF π with π(0) = π(LOG') = 1 together with the lexicographic path order with empty precedence, rule 59 is weakly decreasing and rule 55 is strictly decreasing. There is one new SCC.
- Consider the SCC {59}. By taking the AF π with π(LOG') = 1 together with the lexicographic path order with empty precedence, rule 59 is strictly decreasing.

Tyrolean Termination Tool (0.13 seconds) --- May 4, 2006